A:Type, eq:EqDecider(A), B:(AType), P, Q:(A), f:x:A fp B(x).
filter(pL.Q(pL.1);fpf-vals(eq;P;f)) ~ fpf-vals(eq;a.(P(a))  (Q(a));f) 

latex

Definitions	x. t(x), t  T, x(s), x:A. B(x), t.2, let x = a in b(x), fpf-vals(eq;P;f), t.1, P  Q, P  Q, , {T}, Y, reduce(f;k;as), zip(as;bs), filter(P;l), ff, tt, if b then t else f fi , p  q, map(f;as), a:A fp B(a), P & Q, P  Q, P  Q, Unit, ,
Lemmas	deq wf, bool wf, fpf wf, l member wf, remove-repeats wf, strong-subtype-self, strong-subtype-set3, strong-subtype-deq-subtype, cons member, subtype rel list, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert